e1  e2 == ((e1.1) = (e2.1)) c (e1.2).1 loc (e2.2).1  

latex

---

clarification:

poss-le{i:l}(e1; e2) == ((e1.1) = (e2.1)  ES{i}) c es-le(e1.1;(e1.2).1;(e2.2).1) 

latex

Definitions	A c B, s = t, ES, e loc e' , t.1, t.2
FDL editor aliases	poss-le